module traveldream/agenzia

open traveldream/prodotti
open traveldream/pacchetti

sig Quantita in Int {} {
	this >= 0
}

sig ElementoCarrello {
	pacchetto : one PacchettoPersonalizzato,
	quantita : one Quantita
} {
	quantita > 0
}

sig ElementoGiftlist {
	elemento : one ElementoCarrello,
	regalati : set (Prodotto set -> one Quantita)
} {
	/* I prodotti in "regalati" sono quelli che compongono il pacchetto */
	regalati.Quantita = elemento.pacchetto.(andata + soggiorno + attivita + ritorno)
	/* La quantita regalata è compresa tra 0 e la quantità di pacchetti */
	all q : regalati[Prodotto] | q <= elemento.quantita
	/* Quando è tutto regalato viene tolto dalla giftlist e va in acquisti */
	some q : regalati[Prodotto] | q < elemento.quantita
}

abstract sig Utente {}

some sig Dipendente extends Utente {}

/*Generico utente con una sessione, ma non autenticato come dipendente */
abstract sig UtenteEsterno extends Utente {
	personalizando : lone PacchettoPersonalizzato,
}

sig UtenteAnonimo extends UtenteEsterno {}

sig ClienteRegistrato extends UtenteEsterno {
	carrello : set ElementoCarrello,
	giftlist : set ElementoGiftlist,
	acquisti : set ElementoCarrello
}

sig Catalogo {
	prodotti : set Prodotto,
	pacchetti : set PacchettoPredefinito
} {
	all p : pacchetti | contenuto[p, prodotti]
}

pred inCatalogo [p : PacchettoPersonalizzato, c : Catalogo] {
	p.modello in c.pacchetti
	contenuto[p, c.prodotti]
}

/* In alloy non è modellata la disponibilità effettiva di un prodotto
 * in una specifica data in quanto controllo esterno al sistema */
pred acquistabile [p : PacchettoPersonalizzato, c : Catalogo] {
	!scaduto[p]
 	inCatalogo[p, c]
}

one sig eTravelDream {
	catalogo : one Catalogo,
	utenti : set Utente
} {
	/* Il pacchetto in personalizzazione non più in catalogo viene annullato */
	all p : utenti.personalizando | inCatalogo[p, catalogo]
	/* I pacchetti non più acquistabili vengono tolti da carrello e giftlist */
	all e : utenti.carrello | acquistabile[e.pacchetto, catalogo]
	all e : utenti.giftlist.elemento | acquistabile[e.pacchetto, catalogo]
	/* I pacchetti acquistati rimangono associati all'utente fino alla loro scadenza */
	all e : utenti.acquisti | !scaduto[e.pacchetto]
}

/* Vincoli legati alla natura del sistema */
fact {
	/* Non ha senso l'esistenza di nessun luogo che non sia dipendente da un'altra signature */
	all l : Luogo | l in (Trasporto.(provenienza + destinazione) + Attivita.luogo + Alloggio.luogo + Pacchetto.luogo)
	/* Tutti i prodotti sono o nel catalogo o nei pacchetti */
	all p : Prodotto | p in (Catalogo.prodotti + Pacchetto.(andata + soggiorno + attivita + ritorno))
	/* Tutti i pacchetti predefiniti sono nel catalogo o nei modelli di pacchetti personalizzati */ 
	all p : PacchettoPredefinito | p in (Catalogo.pacchetti + PacchettoPersonalizzato.modello)
	/* Tutti i pacchetti personalizzati sono in modifica o in un elemento di carrello */
	all p : PacchettoPersonalizzato | p in (eTravelDream.utenti.personalizando + ElementoCarrello.pacchetto)
	/* Gli elementi di carrello sono nel carrello, negli acquisti o in elementi in giftlist */
	all e : ElementoCarrello | e in (eTravelDream.utenti.(carrello + acquisti) + ElementoGiftlist.elemento)
	/* Gli elementi della giftlist sono tutti nelle giftlist */
	all e : ElementoGiftlist | e in (eTravelDream.utenti.giftlist)
	/* Si ha solo un catalogo, quello in relazione con l'agenzia */
	all c : Catalogo | c in eTravelDream.catalogo
	/* Tutti gli utenti sono nell'elenco degli utenti */
	all u : Utente | u in eTravelDream.utenti

	/* Non ha senso avere due pacchetti predefiniti equivalenti */
	no disj p1, p2 : PacchettoPredefinito | equivalente[p1, p2]
	/* Consideriamo due pacchetti identici di fatto uno solo */
	no disj p1, p2 : PacchettoPersonalizzato | identico[p1, p2]
}

esempioCompleto: run {
	some UtenteAnonimo
	some carrello
	some giftlist
	some acquisti
} for 10
